Przykładowy dowód w pliku tekstowym
autor: Tomasz Drab (tomasz.drab@cs.uni.wroc.pl)
data: 14 marca 2019 r.
licencja: CC-BY

Pokażemy, że każda liczba naturalna jest parzysta lub nieparzysta.

Formalnie: ∀ n, nat? n ⇒ ( (∃ m, nat? m ∧ n=2*m) ∨ (∃ m, nat? m ∧ n=2*m+1) )

Zasada indukcji dla własności P dla liczb naturalnych:
P 0 ∧ (∀ k, nat? k ∧ P k ⇒ P (k+1)) ⇒ (∀ n, nat? n ⇒ P n)

Pomocniczo przyjmiemy nazwę:
P _ = (∃ m, nat? m ∧ _=2*m) ∨ (∃ m, nat? m ∧ _=2*m+1)

Zatem chcemy udowodnić ∀ n, nat? n ⇒ P n.

Korzystamy z zasady indukcji, więc wystarczy pokazać
P 0 ∧ (∀ k, nat? k ∧ P k ⇒ P (k+1)).

Pokażemy P 0:
  0=2*0, a nawet
  nat? 0 ∧ 0=2*0, więc
   ∃ m, nat? m ∧ 0=2*m, więc
  (∃ m, nat? m ∧ 0=2*m) ∨ (∃ m, nat? m ∧ 0=2*m+1), czyli
  P 0.

Pokażemy (∀ k, nat? k ∧ P k ⇒ P (k+1)):
  Weźmy dowolną liczbę naturalną k i załóżmy P k (że jest parzysta lub
  nieparzysta).
  
    przypadek 1) (jest parzysta)
         ∃ m, nat? m ∧ k=2*m
      Weźmy taką liczbę m.
      Wtedy (k+1)=2*m+1, więc (m jest odpowiednią liczbą)
         ∃ m, nat? m ∧ (k+1)=2*m+1, więc
      (∃ m, nat? m ∧ (k+1)=2*m) ∨ (∃ m, nat? m ∧ (k+1)=2*m+1), czyli
      P (k+1).

    przypadek 2) (jest nieparzysta)
         ∃ m, nat? m ∧ k=2*m+1
      Weźmy taką liczbę m.
      Wtedy (k+1)=2*m+2, czyli
      (k+1)=2*(m+1), więc (m+1 jest odpowiednią liczbą)
         ∃ m, nat? m ∧ (k+1)=2*m, więc
      (∃ m, nat? m ∧ (k+1)=2*m) ∨ (∃ m, nat? m ∧ (k+1)=2*m+1), czyli
      P (k+1).
    
    W obu przypadkach wykazaliśmy P (k+1).
  Z powyższego (∀ k, nat? k ∧ P k ⇒ P (k+1)).

Podsumowując:
Pokazaliśmy P 0 oraz (∀ k, nat? k ∧ P k ⇒ P (k+1)), więc na mocy zasady
indukcji mamy (∀ n, nat? n ⇒ P n), czyli
∀ n, nat? n ⇒ ( (∃ m, nat? m ∧ n=2*m) ∨ (∃ m, nat? m ∧ n=2*m+1) ),
co było do udowodnienia.